1  /-
  2  Copyright (c) 2019 Floris van Doorn. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Floris van Doorn
  5  -/
  6  
  7  import analysis.complex.exponential
src         └──────────────────────────┘
  8  
  9  namespace real
 10  variable (x : ℝ)
 11  
 12  /-- the series `sqrt_two_add_series x n` is `sqrt(2 + sqrt(2 + ... ))` with `n` square roots,
 13    starting with `x`. We define it here because `cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2`
 14  -/
 15  @[simp] noncomputable def sqrt_two_add_series (x : ℝ) : ℕ → ℝ
doc    └──┘
 16  | 0     := x
 17  | (n+1) := sqrt (2 + sqrt_two_add_series n)
 18  
 19  lemma sqrt_two_add_series_zero : sqrt_two_add_series x 0 = x := by simp
 20  lemma sqrt_two_add_series_one : sqrt_two_add_series 0 1 = sqrt 2 := by simp
 21  lemma sqrt_two_add_series_two : sqrt_two_add_series 0 2 = sqrt (2 + sqrt 2) := by simp
 22  
 23  lemma sqrt_two_add_series_zero_nonneg : ∀(n : ℕ), sqrt_two_add_series 0 n ≥ 0
 24  | 0     := le_refl 0
 25  | (n+1) := sqrt_nonneg _
 26  
 27  lemma sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) : ∀(n : ℕ), sqrt_two_add_series x n ≥ 0
 28  | 0     := h
 29  | (n+1) := sqrt_nonneg _
 30  
 31  lemma sqrt_two_add_series_lt_two : ∀(n : ℕ), sqrt_two_add_series 0 n < 2
 32  | 0     := by norm_num
src                └───────┘
typ                └───────┘
doc                └───────┘
txt                └───────┘
par                └───────┘
pid                        
 33  | (n+1) :=
 34    begin
 35      refine lt_of_lt_of_le _ (le_of_eq $ sqrt_sqr $ le_of_lt two_pos),
src      └─────┘              └─┘                                  
typ      └─────┘              └─┘                                  
doc      └─────┘              └─┘                                  
txt      └─────┘              └─┘                                  
par      └─────┘              └─┘                                  
pid                          └─┘                                  
 36      rw [sqrt_two_add_series, sqrt_lt],
id                                 └────┘
src      └──┘                   └┘ └────┘
typ      └──┘                   └┘ └────┘
doc      └──┘                   └┘       
txt      └──┘                   └┘       
par      └──┘                   └┘       
pid        └┘                   └┘       
st                                 └────┘└──
 37      apply add_lt_of_lt_sub_left,
id             └───────────────────┘
src      └────┘└───────────────────┘
typ      └────┘└───────────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────────┘└─
 38      apply lt_of_lt_of_le (sqrt_two_add_series_lt_two n),
id             └────────────┘  └────────────────────────┘ 
src      └────┘└────────────┘                            
typ      └────┘└────────────┘ └────────────────────────┘
doc      └────┘                                          
txt      └────┘                                          
par      └────┘                                          
pid                                                     
st   ──────────────────────────────────────────────────────┘└─
 39      norm_num, apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num
id                       └────────┘                  └─────────────────────────────┘
src      └──────┘  └────┘└────────┘  └──────┘  └────┘└─────────────────────────────┘  └────────
typ      └──────┘  └────┘└────────┘  └──────┘  └────┘└─────────────────────────────┘  └────────
doc      └──────┘  └────┘            └──────┘  └────┘                                 └────────
txt      └──────┘  └────┘            └──────┘  └────┘                                 └────────
par      └──────┘  └────┘            └──────┘  └────┘                                 └────────
pid                                                                                         
st   ───────────┘└────────────────┘└────────┘└─────────────────────────────────────┘└──────────
 40    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
 41  
 42  lemma sqrt_two_add_series_succ (x : ℝ) :
id                                       
src                                      
typ                                      
 43    ∀(n : ℕ), sqrt_two_add_series x (n+1) = sqrt_two_add_series (sqrt (2 + x)) n
id             └─────────────────┘       └─────────────────┘  └──┘        
src             └─────────────────┘         └─────────────────┘  └──┘    
typ            └─────────────────┘       └─────────────────┘  └──┘        
doc              └─────────────────┘           └─────────────────┘
 44  | 0     := rfl
id              └─┘
src             └─┘
typ             └─┘
 45  | (n+1) := by rw [sqrt_two_add_series, sqrt_two_add_series_succ, sqrt_two_add_series]
id                    └─────────────────┘  └──────────────────────┘  └─────────────────┘
src               └──┘└─────────────────┘└┘                        └┘└─────────────────┘└─
typ               └──┘└─────────────────┘└┘└──────────────────────┘└┘└─────────────────┘└─
doc                └──┘└─────────────────┘└┘                        └┘└─────────────────┘└─
txt                └──┘                   └┘                        └┘                   └─
par                └──┘                   └┘                        └┘                   └─
pid                  └┘                   └┘                        └┘                   
st                └──────────────────────┘└────────────────────────┘└───────────────────┘
 46  
src  
typ  
doc  
txt  
par  
pid  
st   
 47  lemma sqrt_two_add_series_monotone_left {x y : ℝ} (h : x ≤ y) :
id                                                           
src                                                          
typ                                                          
 48    ∀(n : ℕ), sqrt_two_add_series x n ≤ sqrt_two_add_series y n
id             └─────────────────┘    └─────────────────┘  
src             └─────────────────┘      └─────────────────┘
typ            └─────────────────┘    └─────────────────┘  
doc              └─────────────────┘       └─────────────────┘
 49  | 0     := h
id              
typ             
 50  | (n+1) :=
id       
src      
typ      
 51    begin
st     └─────
 52      rw [sqrt_two_add_series, sqrt_two_add_series],
id           └─────────────────┘  └─────────────────┘
src      └──┘└─────────────────┘└┘└─────────────────┘
typ      └──┘└─────────────────┘└┘└─────────────────┘
doc      └──┘└─────────────────┘└┘└─────────────────┘
txt      └──┘                   └┘                   
par      └──┘                   └┘                   
pid        └┘                   └┘                   
st   ──────────────────────────┘└───────────────────┘└──
 53      apply sqrt_le_sqrt, apply add_le_add_left, apply sqrt_two_add_series_monotone_left
id             └──────────┘        └─────────────┘
src      └────┘└──────────┘  └────┘└─────────────┘  └────┘                                 
typ      └────┘└──────────┘  └────┘└─────────────┘  └────┘                                 
doc      └────┘              └────┘                 └────┘                                 
txt      └────┘              └────┘                 └────┘                                 
par      └────┘              └────┘                 └────┘                                 
pid                                                                                     
st   ─────────────────────┘└─────────────────────┘└─────────────────────────────────────────
 54    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
 55  
 56  lemma sqrt_two_add_series_step_up {a b n : ℕ} {z : ℝ} (c d : ℕ)
id                                                              
src                                                             
typ                                                             
 57    (hz : sqrt_two_add_series (c/d) n ≤ z) (hb : b ≠ 0) (hd : d ≠ 0)
id           └─────────────────┘                          
src          └─────────────────┘                                
typ          └─────────────────┘                          
doc          └─────────────────┘
 58    (h : (2 * b + a) * d ^ 2 ≤ c ^ 2 * b) : sqrt_two_add_series (a/b) (n+1) ≤ z :=
id                                 └─────────────────┘         
src                                     └─────────────────┘           
typ                                └─────────────────┘         
doc                                            └─────────────────┘
 59  begin
st   └─────
 60    refine le_trans _ hz, rw [sqrt_two_add_series_succ], apply sqrt_two_add_series_monotone_left,
id            └──────┘   └┘      └──────────────────────┘         └───────────────────────────────┘
src    └─────┘└──────┘└─┘    └──┘└──────────────────────┘  └────┘└───────────────────────────────┘
typ    └─────┘└──────┘└─┘└┘  └──┘└──────────────────────┘  └────┘└───────────────────────────────┘
doc    └─────┘        └─┘    └──┘                          └────┘
txt    └─────┘        └─┘    └──┘                          └────┘
par    └─────┘        └─┘    └──┘                          └────┘
pid                  └─┘      └┘                               
st   ─────────────────────┘└────────────────────────────┘└────────────────────────────────────────┘└─
 61    rwa [sqrt_le_left, div_pow, add_div_eq_mul_add_div, div_le_iff, mul_comm (_/_), ←mul_div_assoc,
id          └──────────┘  └─────┘  └────────────────────┘  └────────┘  └──────┘        └───────────┘
src    └───┘└──────────┘└┘└─────┘└┘└────────────────────┘└┘└────────┘└┘└──────┘ └───┘└───────────┘└─
typ    └───┘└──────────┘└┘└─────┘└┘└────────────────────┘└┘└────────┘└┘└──────┘ └───┘└───────────┘└─
doc    └───┘            └┘       └┘                      └┘          └┘          └───┘             └─
txt    └───┘            └┘       └┘                      └┘          └┘          └───┘             └─
par    └───┘            └┘       └┘                      └┘          └┘          └───┘             └─
pid       └┘            └┘       └┘                      └┘          └┘          └───┘             └─
st   ──────────────────┘└───────┘└──────────────────────┘└──────────┘└──────────────┘└──────────────┘└─
 62        le_div_iff, ←nat.cast_pow, ←nat.cast_pow, ←@nat.cast_one ℝ, ←nat.cast_bit0, ←nat.cast_mul,
id         └────────┘   └──────────┘   └──────────┘    └──────────┘     └───────────┘   └──────────┘
src  ─────┘└────────┘└─┘└──────────┘└─┘└──────────┘└─┘ └──────────┘ └─┘└───────────┘└─┘└──────────┘└─
typ  ─────┘└────────┘└─┘└──────────┘└─┘└──────────┘└─┘ └──────────┘ └─┘└───────────┘└─┘└──────────┘└─
doc  ─────┘          └─┘            └─┘            └─┘              └─┘             └─┘            └─
txt  ─────┘          └─┘            └─┘            └─┘              └─┘             └─┘            └─
par  ─────┘          └─┘            └─┘            └─┘              └─┘             └─┘            └─
pid  ─────┘          └─┘            └─┘            └─┘              └─┘             └─┘            └─
st   ───────────────┘└─────────────┘└─────────────┘└────────────────┘└──────────────┘└─────────────┘└─
 63        ←nat.cast_mul, ←nat.cast_add, ←nat.cast_mul, nat.cast_le, mul_comm b],
id          └──────────┘   └──────────┘   └──────────┘  └─────────┘  └──────┘ 
src  ──────┘└──────────┘└─┘└──────────┘└─┘└──────────┘└┘└─────────┘└┘└──────┘ 
typ  ──────┘└──────────┘└─┘└──────────┘└─┘└──────────┘└┘└─────────┘└┘└──────┘
doc  ──────┘            └─┘            └─┘            └┘           └┘         
txt  ──────┘            └─┘            └─┘            └┘           └┘         
par  ──────┘            └─┘            └─┘            └┘           └┘         
pid  ──────┘            └─┘            └─┘            └┘           └┘         
st   ──────────────────┘└─────────────┘└─────────────┘└───────────┘└──────────┘└─
 64    apply pow_pos, iterate 2 {apply nat.cast_pos.2, apply nat.pos_of_ne_zero, assumption},
id           └─────┘                   └──────────┘          └────────────────┘
src    └────┘└─────┘  └─────────┘└────┘└──────────┘└┘└┘└────┘└────────────────┘└┘└────────┘
typ    └────┘└─────┘  └─────────┘└────┘└──────────┘└┘└┘└────┘└────────────────┘└┘└────────┘
doc    └────┘         └─────────┘└────┘            └┘└┘└────┘                  └┘└────────┘
txt    └────┘         └─────────┘└────┘            └┘└┘└────┘                  └┘└────────┘
par    └────┘         └─────────┘└────┘            └┘└┘└────┘                  └┘└────────┘
pid                         └───────┘            └────────┘                  └───────────┘
st   ──────────────┘└───────────────────────────────┘└────────────────────────┘└──────────┘└┘
 65    exact nat.cast_ne_zero.2 hb,
id           └──────────────┘   └┘
src    └────┘└──────────────┘└─┘
typ    └────┘└──────────────┘└─┘└┘
doc    └────┘                └─┘
txt    └────┘                └─┘
par    └────┘                └─┘
pid                         └─┘
st   ────────────────────────────┘└─
 66    exact nat.cast_ne_zero.2 hd,
id           └──────────────┘   └┘
src    └────┘└──────────────┘└─┘
typ    └────┘└──────────────┘└─┘└┘
doc    └────┘                └─┘
txt    └────┘                └─┘
par    └────┘                └─┘
pid                         └─┘
st   ────────────────────────────┘└─
 67    exact div_nonneg (nat.cast_nonneg _) (nat.cast_pos.2 $ nat.pos_of_ne_zero hd)
id           └────────┘  └─────────────┘     └──────────┘     └────────────────┘ └┘
src    └────┘└────────┘ └─────────────┘└──┘ └──────────┘└─┘ └────────────────┘  └┘
typ    └────┘└────────┘ └─────────────┘└──┘ └──────────┘└─┘ └────────────────┘└┘└┘
doc    └────┘                          └──┘             └─┘                     └┘
txt    └────┘                          └──┘             └─┘                     └┘
par    └────┘                          └──┘             └─┘                     └┘
pid                                   └──┘             └─┘                     
st   ───────────────────────────────────────────────────────────────────────────────┘
 68  end
st   └─┘
 69  
 70  lemma sqrt_two_add_series_step_down {c d n : ℕ} {z : ℝ} (a b : ℕ)
id                                                                
src                                                               
typ                                                               
 71    (hz : z ≤ sqrt_two_add_series (a/b) n) (hb : b ≠ 0) (hd : d ≠ 0)
id             └─────────────────┘                        
src             └─────────────────┘                             
typ            └─────────────────┘                        
doc              └─────────────────┘
 72    (h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2) : z ≤ sqrt_two_add_series (c/d) (n+1) :=
id                                   └─────────────────┘     
src                                        └─────────────────┘        
typ                                  └─────────────────┘     
doc                                                └─────────────────┘
 73  begin
st   └─────
 74    apply le_trans hz, rw [sqrt_two_add_series_succ], apply sqrt_two_add_series_monotone_left,
id           └──────┘ └┘      └──────────────────────┘         └───────────────────────────────┘
src    └────┘└──────┘    └──┘└──────────────────────┘  └────┘└───────────────────────────────┘
typ    └────┘└──────┘└┘  └──┘└──────────────────────┘  └────┘└───────────────────────────────┘
doc    └────┘            └──┘                          └────┘
txt    └────┘            └──┘                          └────┘
par    └────┘            └──┘                          └────┘
pid                       └┘                               
st   ──────────────────┘└────────────────────────────┘└────────────────────────────────────────┘└─
 75    apply le_sqrt_of_sqr_le,
id           └───────────────┘
src    └────┘└───────────────┘
typ    └────┘└───────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────────────┘└─
 76    rwa [div_pow, add_div_eq_mul_add_div, div_le_iff, mul_comm (_/_), ←mul_div_assoc,
id          └─────┘  └────────────────────┘  └────────┘  └──────┘        └───────────┘
src    └───┘└─────┘└┘└────────────────────┘└┘└────────┘└┘└──────┘ └───┘└───────────┘└─
typ    └───┘└─────┘└┘└────────────────────┘└┘└────────┘└┘└──────┘ └───┘└───────────┘└─
doc    └───┘       └┘                      └┘          └┘          └───┘             └─
txt    └───┘       └┘                      └┘          └┘          └───┘             └─
par    └───┘       └┘                      └┘          └┘          └───┘             └─
pid       └┘       └┘                      └┘          └┘          └───┘             └─
st   ─────────────┘└──────────────────────┘└──────────┘└──────────────┘└──────────────┘└─
 77        le_div_iff, ←nat.cast_pow, ←nat.cast_pow, ←@nat.cast_one ℝ, ←nat.cast_bit0, ←nat.cast_mul,
id         └────────┘   └──────────┘   └──────────┘    └──────────┘     └───────────┘   └──────────┘
src  ─────┘└────────┘└─┘└──────────┘└─┘└──────────┘└─┘ └──────────┘ └─┘└───────────┘└─┘└──────────┘└─
typ  ─────┘└────────┘└─┘└──────────┘└─┘└──────────┘└─┘ └──────────┘ └─┘└───────────┘└─┘└──────────┘└─
doc  ─────┘          └─┘            └─┘            └─┘              └─┘             └─┘            └─
txt  ─────┘          └─┘            └─┘            └─┘              └─┘             └─┘            └─
par  ─────┘          └─┘            └─┘            └─┘              └─┘             └─┘            └─
pid  ─────┘          └─┘            └─┘            └─┘              └─┘             └─┘            └─
st   ───────────────┘└─────────────┘└─────────────┘└────────────────┘└──────────────┘└─────────────┘└─
 78        ←nat.cast_mul, ←nat.cast_add, ←nat.cast_mul, nat.cast_le, mul_comm (b ^ 2)],
id          └──────────┘   └──────────┘   └──────────┘  └─────────┘  └──────┘   
src  ──────┘└──────────┘└─┘└──────────┘└─┘└──────────┘└┘└─────────┘└┘└──────┘  └──┘
typ  ──────┘└──────────┘└─┘└──────────┘└─┘└──────────┘└┘└─────────┘└┘└──────┘ └──┘
doc  ──────┘            └─┘            └─┘            └┘           └┘           └──┘
txt  ──────┘            └─┘            └─┘            └┘           └┘           └──┘
par  ──────┘            └─┘            └─┘            └┘           └┘           └──┘
pid  ──────┘            └─┘            └─┘            └┘           └┘           └──┘
st   ──────────────────┘└─────────────┘└─────────────┘└───────────┘└────────────────┘└─
 79    swap, apply pow_pos, iterate 2 {apply nat.cast_pos.2, apply nat.pos_of_ne_zero, assumption},
id                 └─────┘                   └──────────┘          └────────────────┘
src    └──┘  └────┘└─────┘  └─────────┘└────┘└──────────┘└┘└┘└────┘└────────────────┘└┘└────────┘
typ    └──┘  └────┘└─────┘  └─────────┘└────┘└──────────┘└┘└┘└────┘└────────────────┘└┘└────────┘
doc    └──┘  └────┘         └─────────┘└────┘            └┘└┘└────┘                  └┘└────────┘
txt    └──┘  └────┘         └─────────┘└────┘            └┘└┘└────┘                  └┘└────────┘
par    └──┘  └────┘         └─────────┘└────┘            └┘└┘└────┘                  └┘└────────┘
pid                               └───────┘            └────────┘                  └───────────┘
st   ─────┘└─────────────┘└───────────────────────────────┘└────────────────────────┘└──────────┘└┘
 80    exact nat.cast_ne_zero.2 hd,
id           └──────────────┘   └┘
src    └────┘└──────────────┘└─┘
typ    └────┘└──────────────┘└─┘└┘
doc    └────┘                └─┘
txt    └────┘                └─┘
par    └────┘                └─┘
pid                         └─┘
st   ────────────────────────────┘└─
 81    exact nat.cast_ne_zero.2 hb
id           └──────────────┘   └┘
src    └────┘└──────────────┘└─┘  
typ    └────┘└──────────────┘└─┘└┘
doc    └────┘                └─┘  
txt    └────┘                └─┘  
par    └────┘                └─┘  
pid                         └─┘  
st   ─────────────────────────────┘
 82  end
st   └─┘
 83  
 84  @[simp] lemma cos_pi_over_two_pow : ∀(n : ℕ), cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2
id                                               └─┘  └┘           └─────────────────┘    
src                                               └─┘  └┘            └─────────────────┘     
typ                                              └─┘  └┘           └─────────────────┘    
doc    └──┘                                             └┘                └─────────────────┘
 85  | 0     := by simp
src                └───┘
typ                └───┘
doc                └───┘
txt                └───┘
par                └───┘
pid                    
st                └────┘
 86  | (n+1) :=
id       
src      
typ      
 87    begin
st     └─────
 88      symmetry, rw [div_eq_iff_mul_eq], symmetry,
id                     └───────────────┘
src      └──────┘  └──┘└───────────────┘  └──────┘
typ      └──────┘  └──┘└───────────────┘  └──────┘
doc      └──────┘  └──┘                   └──────┘
txt      └──────┘  └──┘                   └──────┘
par      └──────┘  └──┘                   └──────┘
pid                  └┘                 
st   ───────────┘└─────────────────────┘└─────────┘└─
 89      rw [sqrt_two_add_series, sqrt_eq_iff_sqr_eq, mul_pow, cos_square, ←mul_div_assoc,
id           └─────────────────┘  └────────────────┘  └─────┘  └────────┘   └───────────┘
src      └──┘└─────────────────┘└┘└────────────────┘└┘└─────┘└┘└────────┘└─┘└───────────┘└─
typ      └──┘└─────────────────┘└┘└────────────────┘└┘└─────┘└┘└────────┘└─┘└───────────┘└─
doc      └──┘└─────────────────┘└┘                  └┘       └┘          └─┘             └─
txt      └──┘                   └┘                  └┘       └┘          └─┘             └─
par      └──┘                   └┘                  └┘       └┘          └─┘             └─
pid        └┘                   └┘                  └┘       └┘          └─┘             └─
st   ──────────────────────────┘└──────────────────┘└───────┘└──────────┘└──────────────┘└─
 90        nat.add_succ, pow_succ, mul_div_mul_left, cos_pi_over_two_pow, add_mul],
id         └──────────┘  └──────┘  └──────────────┘  └─────────────────┘  └─────┘
src  ─────┘└──────────┘└┘└──────┘└┘└──────────────┘└┘                   └┘└─────┘
typ  ─────┘└──────────┘└┘└──────┘└┘└──────────────┘└┘└─────────────────┘└┘└─────┘
doc  ─────┘            └┘        └┘                └┘                   └┘       
txt  ─────┘            └┘        └┘                └┘                   └┘       
par  ─────┘            └┘        └┘                └┘                   └┘       
pid  ─────┘            └┘        └┘                └┘                   └┘       
st   ─────────────────┘└────────┘└────────────────┘└───────────────────┘└───────┘└──
 91      congr, norm_num,
src      └───┘  └──────┘
typ      └───┘  └──────┘
doc             └──────┘
txt      └───┘  └──────┘
par      └───┘  └──────┘
st   ────────┘└────────┘└─
 92      rw [mul_comm, pow_two, mul_assoc, ←mul_div_assoc, mul_div_cancel_left, ←mul_div_assoc,
id           └──────┘  └─────┘  └───────┘   └───────────┘  └─────────────────┘   └───────────┘
src      └──┘└──────┘└┘└─────┘└┘└───────┘└─┘└───────────┘└┘└─────────────────┘└─┘└───────────┘└─
typ      └──┘└──────┘└┘└─────┘└┘└───────┘└─┘└───────────┘└┘└─────────────────┘└─┘└───────────┘└─
doc      └──┘        └┘       └┘         └─┘             └┘                   └─┘             └─
txt      └──┘        └┘       └┘         └─┘             └┘                   └─┘             └─
par      └──┘        └┘       └┘         └─┘             └┘                   └─┘             └─
pid        └┘        └┘       └┘         └─┘             └┘                   └─┘             └─
st   ───────────────┘└───────┘└─────────┘└──────────────┘└───────────────────┘└──────────────┘└─
 93          mul_div_cancel_left],
id           └─────────────────┘
src  ───────┘└─────────────────┘
typ  ───────┘└─────────────────┘
doc  ───────┘                   
txt  ───────┘                   
par  ───────┘                   
pid  ───────┘                   
st   ──────────────────────────┘└──
 94      norm_num, norm_num, apply pow_ne_zero, norm_num, norm_num,
id                                 └─────────┘
src      └──────┘  └──────┘  └────┘└─────────┘  └──────┘  └──────┘
typ      └──────┘  └──────┘  └────┘└─────────┘  └──────┘  └──────┘
doc      └──────┘  └──────┘  └────┘             └──────┘  └──────┘
txt      └──────┘  └──────┘  └────┘             └──────┘  └──────┘
par      └──────┘  └──────┘  └────┘             └──────┘  └──────┘
pid                               
st   ───────────┘└────────┘└─────────────────┘└────────┘└────────┘└─
 95      apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg, norm_num,
id             └────────┘                  └─────────────────────────────┘
src      └────┘└────────┘  └──────┘  └────┘└─────────────────────────────┘  └──────┘
typ      └────┘└────────┘  └──────┘  └────┘└─────────────────────────────┘  └──────┘
doc      └────┘            └──────┘  └────┘                                 └──────┘
txt      └────┘            └──────┘  └────┘                                 └──────┘
par      └────┘            └──────┘  └────┘                                 └──────┘
pid                                      
st   ───────────────────┘└────────┘└─────────────────────────────────────┘└────────┘└─
 96      apply le_of_lt, apply mul_pos, apply cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two,
id             └──────┘        └─────┘        └───────────────────────────────────────────┘
src      └────┘└──────┘  └────┘└─────┘  └────┘└───────────────────────────────────────────┘
typ      └────┘└──────┘  └────┘└─────┘  └────┘└───────────────────────────────────────────┘
doc      └────┘          └────┘         └────┘
txt      └────┘          └────┘         └────┘
par      └────┘          └────┘         └────┘
pid                                        
st   ─────────────────┘└─────────────┘└───────────────────────────────────────────────────┘└─
 97      { transitivity (0 : ℝ), rw neg_lt_zero, apply pi_div_two_pos,
id                                  └─────────┘        └────────────┘
src        └───────────┘ └──┘   └─┘└─────────┘  └────┘└────────────┘
typ        └───────────┘ └──┘   └─┘└─────────┘  └────┘└────────────┘
doc        └───────────┘ └──┘   └─┘             └────┘
txt        └───────────┘ └──┘   └─┘             └────┘
par        └───────────┘ └──┘   └─┘             └────┘
pid                     └──┘                       
st   ─────┘└──────────────────┘└──────────────┘└────────────────────┘└─
 98        apply div_pos pi_pos, apply pow_pos, norm_num },
id               └─────┘ └────┘        └─────┘
src        └────┘└─────┘└────┘  └────┘└─────┘  └───────┘
typ        └────┘└─────┘└────┘  └────┘└─────┘  └───────┘
doc        └────┘               └────┘         └───────┘
txt        └────┘               └────┘         └───────┘
par        └────┘               └────┘         └───────┘
pid                                                  
st   ─────────────────────────┘└─────────────┘└─────────┘└┘
 99      apply div_lt_div' (le_refl pi) _ pi_pos _,
id             └─────────┘  └─────┘ └┘    └────┘
src      └────┘└─────────┘ └─────┘└┘└──┘└────┘└┘
typ      └────┘└─────────┘ └─────┘└┘└──┘└────┘└┘
doc      └────┘                   └┘└──┘      └┘
txt      └────┘                     └──┘      └┘
par      └────┘                     └──┘      └┘
pid                                └──┘      └┘
st   ────────────────────────────────────────────┘└─
100      refine lt_of_le_of_lt (le_of_eq (pow_one _).symm) _,
id              └────────────┘  └──────┘  └─────┘
src      └─────┘└────────────┘ └──────┘ └─────┘└─────────┘
typ      └─────┘└────────────┘ └──────┘ └─────┘└─────────┘
doc      └─────┘                               └─────────┘
txt      └─────┘                               └─────────┘
par      └─────┘                               └─────────┘
pid                                           └─────────┘
st   ──────────────────────────────────────────────────────┘└─
101      apply pow_lt_pow, norm_num, apply nat.succ_lt_succ, apply nat.succ_pos, all_goals {norm_num}
id             └────────┘                  └──────────────┘        └──────────┘
src      └────┘└────────┘  └──────┘  └────┘└──────────────┘  └────┘└──────────┘  └─────────┘└──────┘└─
typ      └────┘└────────┘  └──────┘  └────┘└──────────────┘  └────┘└──────────┘  └─────────┘└──────┘└─
doc      └────┘            └──────┘  └────┘                  └────┘              └─────────┘└──────┘└─
txt      └────┘            └──────┘  └────┘                  └────┘              └─────────┘└──────┘└─
par      └────┘            └──────┘  └────┘                  └────┘              └─────────┘└──────┘└─
pid                                                                                    └─────────┘
st   ───────────────────┘└────────┘└──────────────────────┘└──────────────────┘└───────────┘└──────┘
102    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
103  
104  lemma sin_square_pi_over_two_pow (n : ℕ) :
id                                         
src                                        
typ                                        
105    sin (pi / 2 ^ (n+1)) ^ 2 = 1 - (sqrt_two_add_series 0 n / 2) ^ 2 :=
id     └─┘  └┘                  └─────────────────┘        
src    └─┘  └┘                   └─────────────────┘         
typ    └─┘  └┘                  └─────────────────┘        
doc         └┘                         └─────────────────┘
st                  
106  by rw [sin_square, cos_pi_over_two_pow]
id          └────────┘  └─────────────────┘
src     └──┘└────────┘└┘└─────────────────┘└─
typ     └──┘└────────┘└┘└─────────────────┘└─
doc     └──┘          └┘                   └─
txt     └──┘          └┘                   └─
par     └──┘          └┘                   └─
pid       └┘          └┘                   
st     └─────────────┘└───────────────────┘
107  
src  
typ  
doc  
txt  
par  
pid  
st   
108  lemma sin_square_pi_over_two_pow_succ (n : ℕ) :
id                                              
src                                             
typ                                             
109    sin (pi / 2 ^ (n+2)) ^ 2 = 1 / 2 - sqrt_two_add_series 0 n / 4 :=
id     └─┘  └┘                    └─────────────────┘    
src    └─┘  └┘                     └─────────────────┘     
typ    └─┘  └┘                    └─────────────────┘    
doc         └┘                            └─────────────────┘
110  begin
st   └─────
111    rw [sin_square_pi_over_two_pow, sqrt_two_add_series, div_pow, sqr_sqrt, add_div, ←sub_sub],
id         └────────────────────────┘  └─────────────────┘  └─────┘  └──────┘  └─────┘   └─────┘
src    └──┘└────────────────────────┘└┘└─────────────────┘└┘└─────┘└┘└──────┘└┘└─────┘└─┘└─────┘
typ    └──┘└────────────────────────┘└┘└─────────────────┘└┘└─────┘└┘└──────┘└┘└─────┘└─┘└─────┘
doc    └──┘                          └┘└─────────────────┘└┘       └┘        └┘       └─┘       
txt    └──┘                          └┘                   └┘       └┘        └┘       └─┘       
par    └──┘                          └┘                   └┘       └┘        └┘       └─┘       
pid      └┘                          └┘                   └┘       └┘        └┘       └─┘       
st   ───────────────────────────────┘└───────────────────┘└───────┘└────────┘└───────┘└────────┘└──
112    congr, norm_num, norm_num, apply add_nonneg, norm_num, apply sqrt_two_add_series_zero_nonneg,
id                                      └────────┘                  └─────────────────────────────┘
src    └───┘  └──────┘  └──────┘  └────┘└────────┘  └──────┘  └────┘└─────────────────────────────┘
typ    └───┘  └──────┘  └──────┘  └────┘└────────┘  └──────┘  └────┘└─────────────────────────────┘
doc           └──────┘  └──────┘  └────┘            └──────┘  └────┘
txt    └───┘  └──────┘  └──────┘  └────┘            └──────┘  └────┘
par    └───┘  └──────┘  └──────┘  └────┘            └──────┘  └────┘
pid                                                               
st   ──────┘└────────┘└────────┘└────────────────┘└────────┘└─────────────────────────────────────┘└─
113    norm_num
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid            
st   ──────────┘
114  end
st   └─┘
115  
116  @[simp] lemma sin_pi_over_two_pow_succ (n : ℕ) :
id                                               
src                                              
typ                                              
doc    └──┘
117    sin (pi / 2 ^ (n+2)) = sqrt (2 - sqrt_two_add_series 0 n) / 2 :=
id     └─┘  └┘           └──┘     └─────────────────┘     
src    └─┘  └┘            └──┘     └─────────────────┘      
typ    └─┘  └┘           └──┘     └─────────────────┘     
doc         └┘                          └─────────────────┘
118  begin
st   └─────
119    symmetry, rw [div_eq_iff_mul_eq], symmetry,
id                   └───────────────┘
src    └──────┘  └──┘└───────────────┘  └──────┘
typ    └──────┘  └──┘└───────────────┘  └──────┘
doc    └──────┘  └──┘                   └──────┘
txt    └──────┘  └──┘                   └──────┘
par    └──────┘  └──┘                   └──────┘
pid                └┘                 
st   ─────────┘└─────────────────────┘└─────────┘└─
120    rw [sqrt_eq_iff_sqr_eq, mul_pow, sin_square_pi_over_two_pow_succ, sub_mul],
id         └────────────────┘  └─────┘  └─────────────────────────────┘  └─────┘
src    └──┘└────────────────┘└┘└─────┘└┘└─────────────────────────────┘└┘└─────┘
typ    └──┘└────────────────┘└┘└─────┘└┘└─────────────────────────────┘└┘└─────┘
doc    └──┘                  └┘       └┘                               └┘       
txt    └──┘                  └┘       └┘                               └┘       
par    └──┘                  └┘       └┘                               └┘       
pid      └┘                  └┘       └┘                               └┘       
st   ───────────────────────┘└───────┘└───────────────────────────────┘└───────┘└──
121    { congr, norm_num, rw [mul_comm], convert mul_div_cancel' _ _, norm_num, norm_num },
id                            └──────┘           └─────────────┘
src      └───┘  └──────┘  └──┘└──────┘  └──────┘└─────────────┘└──┘  └──────┘  └───────┘
typ      └───┘  └──────┘  └──┘└──────┘  └──────┘└─────────────┘└──┘  └──────┘  └───────┘
doc             └──────┘  └──┘          └──────┘               └──┘  └──────┘  └───────┘
txt      └───┘  └──────┘  └──┘          └──────┘               └──┘  └──────┘  └───────┘
par      └───┘  └──────┘  └──┘          └──────┘               └──┘  └──────┘  └───────┘
pid                         └┘                                └──┘                    
st   ───┘└───┘└────────┘└────────────┘└────────────────────────────┘└────────┘└─────────┘└┘
122    { rw [sub_nonneg], apply le_of_lt, apply sqrt_two_add_series_lt_two },
id           └────────┘         └──────┘        └────────────────────────┘
src      └──┘└────────┘  └────┘└──────┘  └────┘└────────────────────────┘
typ      └──┘└────────┘  └────┘└──────┘  └────┘└────────────────────────┘
doc      └──┘            └────┘          └────┘                          
txt      └──┘            └────┘          └────┘                          
par      └──┘            └────┘          └────┘                          
pid        └┘                                                          
st   ───┘└────────────┘└───────────────┘└─────────────────────────────────┘└┘
123    apply le_of_lt, apply mul_pos, apply sin_pos_of_pos_of_lt_pi,
id           └──────┘        └─────┘        └─────────────────────┘
src    └────┘└──────┘  └────┘└─────┘  └────┘└─────────────────────┘
typ    └────┘└──────┘  └────┘└─────┘  └────┘└─────────────────────┘
doc    └────┘          └────┘         └────┘
txt    └────┘          └────┘         └────┘
par    └────┘          └────┘         └────┘
pid                                      
st   ───────────────┘└─────────────┘└─────────────────────────────┘└─
124    { apply div_pos pi_pos, apply pow_pos, norm_num },
id             └─────┘ └────┘        └─────┘
src      └────┘└─────┘└────┘  └────┘└─────┘  └───────┘
typ      └────┘└─────┘└────┘  └────┘└─────┘  └───────┘
doc      └────┘               └────┘         └───────┘
txt      └────┘               └────┘         └───────┘
par      └────┘               └────┘         └───────┘
pid                                                
st   ───┘└──────────────────┘└─────────────┘└─────────┘└┘
125    refine lt_of_lt_of_le _ (le_of_eq (div_one _)), rw [div_lt_div_left],
id            └────────────┘    └──────┘  └─────┘          └─────────────┘
src    └─────┘└────────────┘└─┘ └──────┘ └─────┘└──┘  └──┘└─────────────┘
typ    └─────┘└────────────┘└─┘ └──────┘ └─────┘└──┘  └──┘└─────────────┘
doc    └─────┘              └─┘                 └──┘  └──┘               
txt    └─────┘              └─┘                 └──┘  └──┘               
par    └─────┘              └─┘                 └──┘  └──┘               
pid                        └─┘                 └──┘    └┘               
st   ───────────────────────────────────────────────┘└───────────────────┘└──
126    refine lt_of_le_of_lt (le_of_eq (pow_zero 2).symm) _,
id            └────────────┘  └──────┘  └──────┘
src    └─────┘└────────────┘ └──────┘ └──────┘└─────────┘
typ    └─────┘└────────────┘ └──────┘ └──────┘└─────────┘
doc    └─────┘                                └─────────┘
txt    └─────┘                                └─────────┘
par    └─────┘                                └─────────┘
pid                                          └─────────┘
st   ─────────────────────────────────────────────────────┘└─
127    apply pow_lt_pow, norm_num, apply nat.succ_pos, apply pi_pos,
id           └────────┘                  └──────────┘        └────┘
src    └────┘└────────┘  └──────┘  └────┘└──────────┘  └────┘└────┘
typ    └────┘└────────┘  └──────┘  └────┘└──────────┘  └────┘└────┘
doc    └────┘            └──────┘  └────┘              └────┘
txt    └────┘            └──────┘  └────┘              └────┘
par    └────┘            └──────┘  └────┘              └────┘
pid                                                       
st   ─────────────────┘└────────┘└──────────────────┘└────────────┘└─
128    apply pow_pos, all_goals {norm_num}
id           └─────┘
src    └────┘└─────┘  └─────────┘└──────┘└┘
typ    └────┘└─────┘  └─────────┘└──────┘└┘
doc    └────┘         └─────────┘└──────┘└┘
txt    └────┘         └─────────┘└──────┘└┘
par    └────┘         └─────────┘└──────┘└┘
pid                           └─────────┘
st   ──────────────┘└───────────┘└──────┘
129  end
st   └─┘
130  
131  lemma cos_pi_div_four : cos (pi / 4) = sqrt 2 / 2 :=
id                           └─┘  └┘      └──┘   
src                          └─┘  └┘      └──┘   
typ                          └─┘  └┘      └──┘   
doc                               └┘
132  by { transitivity cos (pi / 2 ^ 2), congr, norm_num, simp }
id                     └─┘  └┘    
src       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
typ       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
doc       └───────────┘    └┘ └─┘ └─┘         └──────┘  └───┘
txt       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
par       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
pid                          └─┘ └─┘                       
st     └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
133  
134  lemma sin_pi_div_four : sin (pi / 4) = sqrt 2 / 2 :=
id                           └─┘  └┘      └──┘   
src                          └─┘  └┘      └──┘   
typ                          └─┘  └┘      └──┘   
doc                               └┘
135  by { transitivity sin (pi / 2 ^ 2), congr, norm_num, simp }
id                     └─┘  └┘    
src       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
typ       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
doc       └───────────┘    └┘ └─┘ └─┘         └──────┘  └───┘
txt       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
par       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
pid                          └─┘ └─┘                       
st     └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
136  
137  lemma cos_pi_div_eight : cos (pi / 8) = sqrt (2 + sqrt 2) / 2 :=
id                            └─┘  └┘      └──┘     └──┘    
src                           └─┘  └┘      └──┘     └──┘    
typ                           └─┘  └┘      └──┘     └──┘    
doc                                └┘
138  by { transitivity cos (pi / 2 ^ 3), congr, norm_num, simp }
id                     └─┘  └┘    
src       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
typ       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
doc       └───────────┘    └┘ └─┘ └─┘         └──────┘  └───┘
txt       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
par       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
pid                          └─┘ └─┘                       
st     └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
139  
140  lemma sin_pi_div_eight : sin (pi / 8) = sqrt (2 - sqrt 2) / 2 :=
id                            └─┘  └┘      └──┘     └──┘    
src                           └─┘  └┘      └──┘     └──┘    
typ                           └─┘  └┘      └──┘     └──┘    
doc                                └┘
141  by { transitivity sin (pi / 2 ^ 3), congr, norm_num, simp }
id                     └─┘  └┘    
src       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
typ       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
doc       └───────────┘    └┘ └─┘ └─┘         └──────┘  └───┘
txt       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
par       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
pid                          └─┘ └─┘                       
st     └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
142  
143  lemma cos_pi_div_sixteen : cos (pi / 16) = sqrt (2 + sqrt (2 + sqrt 2)) / 2 :=
id                              └─┘  └┘       └──┘     └──┘     └──┘     
src                             └─┘  └┘       └──┘     └──┘     └──┘     
typ                             └─┘  └┘       └──┘     └──┘     └──┘     
doc                                  └┘
144  by { transitivity cos (pi / 2 ^ 4), congr, norm_num, simp }
id                     └─┘  └┘    
src       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
typ       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
doc       └───────────┘    └┘ └─┘ └─┘         └──────┘  └───┘
txt       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
par       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
pid                          └─┘ └─┘                       
st     └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
145  
146  lemma sin_pi_div_sixteen : sin (pi / 16) = sqrt (2 - sqrt (2 + sqrt 2)) / 2 :=
id                              └─┘  └┘       └──┘     └──┘     └──┘     
src                             └─┘  └┘       └──┘     └──┘     └──┘     
typ                             └─┘  └┘       └──┘     └──┘     └──┘     
doc                                  └┘
147  by { transitivity sin (pi / 2 ^ 4), congr, norm_num, simp }
id                     └─┘  └┘    
src       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
typ       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
doc       └───────────┘    └┘ └─┘ └─┘         └──────┘  └───┘
txt       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
par       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
pid                          └─┘ └─┘                       
st     └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
148  
149  lemma cos_pi_div_thirty_two : cos (pi / 32) = sqrt (2 + sqrt (2 + sqrt (2 + sqrt 2))) / 2 :=
id                                 └─┘  └┘       └──┘     └──┘     └──┘     └──┘      
src                                └─┘  └┘       └──┘     └──┘     └──┘     └──┘      
typ                                └─┘  └┘       └──┘     └──┘     └──┘     └──┘      
doc                                     └┘
150  by { transitivity cos (pi / 2 ^ 5), congr, norm_num, simp }
id                     └─┘  └┘    
src       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
typ       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
doc       └───────────┘    └┘ └─┘ └─┘         └──────┘  └───┘
txt       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
par       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
pid                          └─┘ └─┘                       
st     └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
151  
152  lemma sin_pi_div_thirty_two : sin (pi / 32) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2 :=
id                                 └─┘  └┘       └──┘     └──┘     └──┘     └──┘      
src                                └─┘  └┘       └──┘     └──┘     └──┘     └──┘      
typ                                └─┘  └┘       └──┘     └──┘     └──┘     └──┘      
doc                                     └┘
153  by { transitivity sin (pi / 2 ^ 5), congr, norm_num, simp }
id                     └─┘  └┘    
src       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
typ       └───────────┘└─┘ └┘└─┘└─┘  └───┘  └──────┘  └───┘
doc       └───────────┘    └┘ └─┘ └─┘         └──────┘  └───┘
txt       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
par       └───────────┘       └─┘ └─┘  └───┘  └──────┘  └───┘
pid                          └─┘ └─┘                       
st     └──────────────────────────────┘└─────┘└────────┘└─────┘└┘
154  
155  lemma pi_gt_sqrt_two_add_series (n : ℕ) : pi > 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) :=
id                                            └┘          └──┘     └─────────────────┘   
src                                           └┘           └──┘     └─────────────────┘
typ                                           └┘          └──┘     └─────────────────┘   
doc                                            └┘                         └─────────────────┘
156  begin
st   └─────
157    have : pi > sqrt (2 - sqrt_two_add_series 0 n) / 2 * 2 ^ (n+2),
id            └┘  └──┘     └─────────────────┘              
src    └─────┘└┘└──┘ └┘└─────────────────┘└─┘ └┘└─┘└─┘  └┘
typ    └─────┘└┘└──┘ └┘└─────────────────┘└─┘ └┘└─┘└─┘ └┘
doc    └─────┘└┘      └┘ └─────────────────┘└─┘ └┘ └─┘ └─┘    └┘
txt    └─────┘        └┘                    └─┘ └┘ └─┘ └─┘    └┘
par    └─────┘        └┘                    └─┘ └┘ └─┘ └─┘    └┘
pid    └───┘└┘        └┘                    └─┘ └┘ └─┘ └─┘    └┘
st   ───────────────────────────────────────────────────────────────┘└─
158    { apply mul_lt_of_lt_div, apply pow_pos, norm_num,
id             └──────────────┘        └─────┘
src      └────┘└──────────────┘  └────┘└─────┘  └──────┘
typ      └────┘└──────────────┘  └────┘└─────┘  └──────┘
doc      └────┘                  └────┘         └──────┘
txt      └────┘                  └────┘         └──────┘
par      └────┘                  └────┘         └──────┘
pid                                  
st   ───┘└────────────────────┘└─────────────┘└────────┘└─
159      rw [←sin_pi_over_two_pow_succ], apply sin_lt, apply div_pos pi_pos, apply pow_pos, norm_num },
id            └──────────────────────┘         └────┘        └─────┘ └────┘        └─────┘
src      └───┘└──────────────────────┘  └────┘└────┘  └────┘└─────┘└────┘  └────┘└─────┘  └───────┘
typ      └───┘└──────────────────────┘  └────┘└────┘  └────┘└─────┘└────┘  └────┘└─────┘  └───────┘
doc      └───┘                          └────┘        └────┘               └────┘         └───────┘
txt      └───┘                          └────┘        └────┘               └────┘         └───────┘
par      └───┘                          └────┘        └────┘               └────┘         └───────┘
pid        └─┘                                                                                 
st   ────────────────────────────────┘└─────────────┘└────────────────────┘└─────────────┘└─────────┘└┘
160    apply lt_of_le_of_lt (le_of_eq _) this,
id           └────────────┘  └──────┘    └──┘
src    └────┘└────────────┘ └──────┘└──┘
typ    └────┘└────────────┘ └──────┘└──┘└──┘
doc    └────┘                       └──┘
txt    └────┘                       └──┘
par    └────┘                       └──┘
pid                                └──┘
st   ───────────────────────────────────────┘└─
161    rw [pow_succ _ (n+1), ←mul_assoc, div_mul_cancel, mul_comm], norm_num
id         └──────┘          └───────┘  └────────────┘  └──────┘
src    └──┘└──────┘└─┘   └───┘└───────┘└┘└────────────┘└┘└──────┘  └───────┘
typ    └──┘└──────┘└─┘  └───┘└───────┘└┘└────────────┘└┘└──────┘  └───────┘
doc    └──┘        └─┘   └───┘         └┘              └┘          └───────┘
txt    └──┘        └─┘   └───┘         └┘              └┘          └───────┘
par    └──┘        └─┘   └───┘         └┘              └┘          └───────┘
pid      └┘        └─┘   └───┘         └┘              └┘                  
st   ─────────────────────┘└──────────┘└──────────────┘└────────┘└──────────┘
162  end
st   └─┘
163  
164  lemma pi_lt_sqrt_two_add_series (n : ℕ) :
id                                        
src                                       
typ                                       
165    pi < 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) + 1 / 4 ^ n :=
id     └┘          └──┘     └─────────────────┘            
src    └┘           └──┘     └─────────────────┘            
typ    └┘          └──┘     └─────────────────┘            
doc    └┘                         └─────────────────┘
166  begin
st   └─────
167    have : pi < (sqrt (2 - sqrt_two_add_series 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * 2 ^ (n+2),
id            └┘   └──┘     └─────────────────┘                                    
src    └─────┘└┘ └──┘ └┘└─────────────────┘└─┘ └┘└─┘└─┘  └┘ └┘ └─┘ └──┘└─┘    └┘
typ    └─────┘└┘ └──┘ └┘└─────────────────┘└─┘ └┘└─┘└─┘  └┘ └┘ └─┘ └──┘└─┘   └┘
doc    └─────┘└┘       └┘ └─────────────────┘└─┘ └┘ └─┘ └─┘  └┘  └┘ └─┘ └──┘ └─┘    └┘
txt    └─────┘         └┘                    └─┘ └┘ └─┘ └─┘  └┘  └┘ └─┘ └──┘ └─┘    └┘
par    └─────┘         └┘                    └─┘ └┘ └─┘ └─┘  └┘  └┘ └─┘ └──┘ └─┘    └┘
pid    └───┘└┘         └┘                    └─┘ └┘ └─┘ └─┘  └┘  └┘ └─┘ └──┘ └─┘    └┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
168    { rw [←div_lt_iff, ←sin_pi_over_two_pow_succ],
id            └────────┘   └──────────────────────┘
src      └───┘└────────┘└─┘└──────────────────────┘
typ      └───┘└────────┘└─┘└──────────────────────┘
doc      └───┘          └─┘                        
txt      └───┘          └─┘                        
par      └───┘          └─┘                        
pid        └─┘          └─┘                        
st   ───┘└─────────────┘└─────────────────────────┘└──
169      refine lt_of_lt_of_le (lt_add_of_sub_right_lt (sin_gt_sub_cube _ _)) _,
id              └────────────┘  └────────────────────┘  └─────────────┘
src      └─────┘└────────────┘ └────────────────────┘ └─────────────┘└──────┘
typ      └─────┘└────────────┘ └────────────────────┘ └─────────────┘└──────┘
doc      └─────┘                                                     └──────┘
txt      └─────┘                                                     └──────┘
par      └─────┘                                                     └──────┘
pid                                                                 └──────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
170      { apply div_pos pi_pos, apply pow_pos, norm_num },
id               └─────┘ └────┘        └─────┘
src        └────┘└─────┘└────┘  └────┘└─────┘  └───────┘
typ        └────┘└─────┘└────┘  └────┘└─────┘  └───────┘
doc        └────┘               └────┘         └───────┘
txt        └────┘               └────┘         └───────┘
par        └────┘               └────┘         └───────┘
pid                                                  
st   ─────┘└──────────────────┘└─────────────┘└─────────┘└┘
171      { apply div_le_of_le_mul, apply pow_pos, norm_num, refine le_trans pi_le_four _,
id               └──────────────┘        └─────┘                   └──────┘ └────────┘
src        └────┘└──────────────┘  └────┘└─────┘  └──────┘  └─────┘└──────┘└────────┘└┘
typ        └────┘└──────────────┘  └────┘└─────┘  └──────┘  └─────┘└──────┘└────────┘└┘
doc        └────┘                  └────┘         └──────┘  └─────┘                  └┘
txt        └────┘                  └────┘         └──────┘  └─────┘                  └┘
par        └────┘                  └────┘         └──────┘  └─────┘                  └┘
pid                                                                               └┘
st   ─────┘└────────────────────┘└─────────────┘└────────┘└────────────────────────────┘└─
172        simp only [show ((4 : ℝ) = 2 ^ 2), by norm_num, mul_one],
id                                                        └─────┘
src        └─────────┘      └──┘ └┘└─┘ └──────┘└──────┘└┘└─────┘
typ        └─────────┘      └──┘ └┘└─┘ └──────┘└──────┘└┘└─────┘
doc        └─────────┘      └──┘ └┘ └─┘ └──────┘└──────┘└┘       
txt        └─────────┘      └──┘ └┘ └─┘ └──────┘└──────┘└┘       
par        └─────────┘      └──┘ └┘ └─┘ └──────┘└──────┘└┘       
pid            └──┘└┘      └──┘ └┘ └─┘ └────────────────┘       
st   ──────────────────────────────────────────┘└───────┘└────────┘└─
173        apply pow_le_pow, norm_num, apply le_add_of_nonneg_left, apply nat.zero_le },
id               └────────┘                  └───────────────────┘        └─────────┘
src        └────┘└────────┘  └──────┘  └────┘└───────────────────┘  └────┘└─────────┘
typ        └────┘└────────┘  └──────┘  └────┘└───────────────────┘  └────┘└─────────┘
doc        └────┘            └──────┘  └────┘                       └────┘           
txt        └────┘            └──────┘  └────┘                       └────┘           
par        └────┘            └──────┘  └────┘                       └────┘           
pid                                                                               
st   ─────────────────────┘└────────┘└───────────────────────────┘└──────────────────┘└┘
174      apply add_le_add_left, rw div_le_div_right,
id             └─────────────┘     └──────────────┘
src      └────┘└─────────────┘  └─┘└──────────────┘
typ      └────┘└─────────────┘  └─┘└──────────────┘
doc      └────┘                 └─┘
txt      └────┘                 └─┘
par      └────┘                 └─┘
pid                              
st   ────────────────────────┘└───────────────────┘└─
175      apply le_div_of_mul_le, apply pow_pos, apply pow_pos, norm_num,
id             └──────────────┘        └─────┘        └─────┘
src      └────┘└──────────────┘  └────┘└─────┘  └────┘└─────┘  └──────┘
typ      └────┘└──────────────┘  └────┘└─────┘  └────┘└─────┘  └──────┘
doc      └────┘                  └────┘         └────┘         └──────┘
txt      └────┘                  └────┘         └────┘         └──────┘
par      └────┘                  └────┘         └────┘         └──────┘
pid                                                
st   ─────────────────────────┘└─────────────┘└─────────────┘└────────┘└─
176      rw [←mul_pow],
id            └─────┘
src      └───┘└─────┘
typ      └───┘└─────┘
doc      └───┘       
txt      └───┘       
par      └───┘       
pid        └─┘       
st   ───────────────┘└──
177      refine le_trans _ (le_of_eq (one_pow 3)), apply pow_le_pow_of_le_left,
id              └──────┘    └──────┘  └─────┘            └───────────────────┘
src      └─────┘└──────┘└─┘ └──────┘ └─────┘└──┘  └────┘└───────────────────┘
typ      └─────┘└──────┘└─┘ └──────┘ └─────┘└──┘  └────┘└───────────────────┘
doc      └─────┘        └─┘                 └──┘  └────┘
txt      └─────┘        └─┘                 └──┘  └────┘
par      └─────┘        └─┘                 └──┘  └────┘
pid                    └─┘                 └──┘       
st   ───────────────────────────────────────────┘└───────────────────────────┘└─
178      { apply le_of_lt, apply mul_pos, apply div_pos pi_pos, apply pow_pos, norm_num, apply pow_pos,
id               └──────┘        └─────┘        └─────┘ └────┘        └─────┘                  └─────┘
src        └────┘└──────┘  └────┘└─────┘  └────┘└─────┘└────┘  └────┘└─────┘  └──────┘  └────┘└─────┘
typ        └────┘└──────┘  └────┘└─────┘  └────┘└─────┘└────┘  └────┘└─────┘  └──────┘  └────┘└─────┘
doc        └────┘          └────┘         └────┘               └────┘         └──────┘  └────┘
txt        └────┘          └────┘         └────┘               └────┘         └──────┘  └────┘
par        └────┘          └────┘         └────┘               └────┘         └──────┘  └────┘
pid                                                                                      
st   ─────┘└────────────┘└─────────────┘└────────────────────┘└─────────────┘└────────┘└─────────────┘└─
179        norm_num },
src        └───────┘
typ        └───────┘
doc        └───────┘
txt        └───────┘
par        └───────┘
pid                
st   ──────────────┘└┘
180      apply mul_le_of_le_div, apply pow_pos, norm_num,
id             └──────────────┘        └─────┘
src      └────┘└──────────────┘  └────┘└─────┘  └──────┘
typ      └────┘└──────────────┘  └────┘└─────┘  └──────┘
doc      └────┘                  └────┘         └──────┘
txt      └────┘                  └────┘         └──────┘
par      └────┘                  └────┘         └──────┘
pid                                  
st   ─────────────────────────┘└─────────────┘└────────┘└─
181      refine le_trans ((div_le_div_right _).mpr pi_le_four) _, apply pow_pos, norm_num,
id              └──────┘   └──────────────┘        └────────┘           └─────┘
src      └─────┘└──────┘  └──────────────┘└──────┘└────────┘└─┘  └────┘└─────┘  └──────┘
typ      └─────┘└──────┘  └──────────────┘└──────┘└────────┘└─┘  └────┘└─────┘  └──────┘
doc      └─────┘                          └──────┘          └─┘  └────┘         └──────┘
txt      └─────┘                          └──────┘          └─┘  └────┘         └──────┘
par      └─────┘                          └──────┘          └─┘  └────┘         └──────┘
pid                                      └──────┘          └─┘       
st   ──────────────────────────────────────────────────────────┘└─────────────┘└────────┘└─
182      rw [pow_succ, pow_succ, ←mul_assoc, ←field.div_div_eq_div_mul],
id           └──────┘  └──────┘   └───────┘   └──────────────────────┘
src      └──┘└──────┘└┘└──────┘└─┘└───────┘└─┘└──────────────────────┘
typ      └──┘└──────┘└┘└──────┘└─┘└───────┘└─┘└──────────────────────┘
doc      └──┘        └┘        └─┘         └─┘                        
txt      └──┘        └┘        └─┘         └─┘                        
par      └──┘        └┘        └─┘         └─┘                        
pid        └┘        └┘        └─┘         └─┘                        
st   ───────────────┘└────────┘└──────────┘└─────────────────────────┘└──
183      convert le_refl _, norm_num, norm_num, apply pow_ne_zero, norm_num, norm_num,
id               └─────┘                              └─────────┘
src      └──────┘└─────┘└┘  └──────┘  └──────┘  └────┘└─────────┘  └──────┘  └──────┘
typ      └──────┘└─────┘└┘  └──────┘  └──────┘  └────┘└─────────┘  └──────┘  └──────┘
doc      └──────┘       └┘  └──────┘  └──────┘  └────┘             └──────┘  └──────┘
txt      └──────┘       └┘  └──────┘  └──────┘  └────┘             └──────┘  └──────┘
par      └──────┘       └┘  └──────┘  └──────┘  └────┘             └──────┘  └──────┘
pid                    └┘                           
st   ────────────────────┘└────────┘└────────┘└─────────────────┘└────────┘└────────┘└─
184      apply pow_pos, norm_num },
id             └─────┘
src      └────┘└─────┘  └───────┘
typ      └────┘└─────┘  └───────┘
doc      └────┘         └───────┘
txt      └────┘         └───────┘
par      └────┘         └───────┘
pid                            
st   ────────────────┘└─────────┘└┘
185    apply lt_of_lt_of_le this (le_of_eq _), rw [add_mul], congr' 1,
id           └────────────┘ └──┘  └──────┘         └─────┘
src    └────┘└────────────┘     └──────┘└─┘  └──┘└─────┘  └──────┘
typ    └────┘└────────────┘└──┘ └──────┘└─┘  └──┘└─────┘  └──────┘
doc    └────┘                           └─┘  └──┘         └──────┘
txt    └────┘                           └─┘  └──┘         └──────┘
par    └────┘                           └─┘  └──┘         └──────┘
pid                                    └─┘    └┘               
st   ───────────────────────────────────────┘└───────────┘└─────────┘└─
186    { rw [pow_succ _ (n+1), ←mul_assoc, div_mul_cancel, mul_comm], norm_num },
id           └──────┘          └───────┘  └────────────┘  └──────┘
src      └──┘└──────┘└─┘   └───┘└───────┘└┘└────────────┘└┘└──────┘  └───────┘
typ      └──┘└──────┘└─┘  └───┘└───────┘└┘└────────────┘└┘└──────┘  └───────┘
doc      └──┘        └─┘   └───┘         └┘              └┘          └───────┘
txt      └──┘        └─┘   └───┘         └┘              └┘          └───────┘
par      └──┘        └─┘   └───┘         └┘              └┘          └───────┘
pid        └┘        └─┘   └───┘         └┘              └┘                  
st   ───┘└──────────────────┘└──────────┘└──────────────┘└────────┘└──────────┘└┘
187    rw [pow_succ, ←pow_mul, mul_comm n 2, pow_mul, show (2 : ℝ) ^ 2 = 4, by norm_num, pow_succ,
id         └──────┘   └─────┘  └──────┘     └─────┘                                    └──────┘
src    └──┘└──────┘└─┘└─────┘└┘└──────┘ └──┘└─────┘└┘     └──┘ └┘ └─┘ └─────┘└──────┘└┘└──────┘└─
typ    └──┘└──────┘└─┘└─────┘└┘└──────┘└──┘└─────┘└┘     └──┘ └┘ └─┘└─────┘└──────┘└┘└──────┘└─
doc    └──┘        └─┘       └┘         └──┘       └┘     └──┘ └┘ └─┘ └─────┘└──────┘└┘        └─
txt    └──┘        └─┘       └┘         └──┘       └┘     └──┘ └┘ └─┘ └─────┘└──────┘└┘        └─
par    └──┘        └─┘       └┘         └──┘       └┘     └──┘ └┘ └─┘ └─────┘└──────┘└┘        └─
pid      └┘        └─┘       └┘         └──┘       └┘     └──┘ └┘ └─┘ └───────────────┘        └─
st   ─────────────┘└────────┘└───────────┘└────────┘└────────────────────────┘└───────┘└────────┘└─
188        pow_succ, ←mul_assoc (2 : ℝ), show (2 : ℝ) * 2 = 4, by norm_num, ←mul_assoc, div_mul_cancel,
id         └──────┘   └───────┘                                             └───────┘  └────────────┘
src  ─────┘└──────┘└─┘└───────┘ └──┘ └─┘     └──┘ └┘ └─┘ └─────┘└──────┘└─┘└───────┘└┘└────────────┘└─
typ  ─────┘└──────┘└─┘└───────┘ └──┘ └─┘     └──┘ └┘ └─┘└─────┘└──────┘└─┘└───────┘└┘└────────────┘└─
doc  ─────┘        └─┘          └──┘ └─┘     └──┘ └┘ └─┘ └─────┘└──────┘└─┘         └┘              └─
txt  ─────┘        └─┘          └──┘ └─┘     └──┘ └┘ └─┘ └─────┘└──────┘└─┘         └┘              └─
par  ─────┘        └─┘          └──┘ └─┘     └──┘ └┘ └─┘ └─────┘└──────┘└─┘         └┘              └─
pid  ─────┘        └─┘          └──┘ └─┘     └──┘ └┘ └─┘ └────────────────┘         └┘              └─
st   ─────────────┘└──────────────────┘└────────────────────────┘└───────┘└──────────┘└──────────────┘└─
189        mul_comm ((2 : ℝ) ^ n), ←div_div_eq_div_mul, div_mul_cancel],
id         └──────┘                └────────────────┘  └────────────┘
src  ─────┘└──────┘  └──┘ └┘  └──┘└────────────────┘└┘└────────────┘
typ  ─────┘└──────┘  └──┘ └┘ └──┘└────────────────┘└┘└────────────┘
doc  ─────┘          └──┘ └┘  └──┘                  └┘              
txt  ─────┘          └──┘ └┘  └──┘                  └┘              
par  ─────┘          └──┘ └┘  └──┘                  └┘              
pid  ─────┘          └──┘ └┘  └──┘                  └┘              
st   ───────────────────────────┘└───────────────────┘└──────────────┘└──
190    apply pow_ne_zero, norm_num, norm_num
id           └─────────┘
src    └────┘└─────────┘  └──────┘  └───────┘
typ    └────┘└─────────┘  └──────┘  └───────┘
doc    └────┘             └──────┘  └───────┘
txt    └────┘             └──────┘  └───────┘
par    └────┘             └──────┘  └───────┘
pid                                        
st   ──────────────────┘└────────┘└─────────┘
191  end
st   └─┘
192  
193  lemma pi_gt_three : pi > 3 :=
id                       └┘ 
src                      └┘ 
typ                      └┘ 
doc                      └┘
194  begin
st   └─────
195    refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series 1), rw [mul_comm],
id            └────────────┘    └───────────────────────┘         └──────┘
src    └─────┘└────────────┘└─┘ └───────────────────────┘└─┘  └──┘└──────┘
typ    └─────┘└────────────┘└─┘ └───────────────────────┘└─┘  └──┘└──────┘
doc    └─────┘              └─┘                          └─┘  └──┘        
txt    └─────┘              └─┘                          └─┘  └──┘        
par    └─────┘              └─┘                          └─┘  └──┘        
pid                        └─┘                          └─┘    └┘        
st   ──────────────────────────────────────────────────────┘└────────────┘└──
196    apply le_mul_of_div_le, norm_num, apply le_sqrt_of_sqr_le, rw [le_sub],
id           └──────────────┘                  └───────────────┘      └────┘
src    └────┘└──────────────┘  └──────┘  └────┘└───────────────┘  └──┘└────┘
typ    └────┘└──────────────┘  └──────┘  └────┘└───────────────┘  └──┘└────┘
doc    └────┘                  └──────┘  └────┘                   └──┘      
txt    └────┘                  └──────┘  └────┘                   └──┘      
par    └────┘                  └──────┘  └────┘                   └──┘      
pid                                                               └┘      
st   ───────────────────────┘└────────┘└───────────────────────┘└──────────┘└──
197    rw show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div],
id                                       └───────────┘  └──────┘
src    └─┘     └┘ └┘ └┘  └┘ └────────┘└───────────┘└┘└──────┘
typ    └─┘     └┘ └┘ └┘  └┘ └────────┘└───────────┘└┘└──────┘
doc    └─┘     └┘ └┘  └┘   └┘ └────────┘             └┘        
txt    └─┘     └┘ └┘  └┘   └┘ └────────┘             └┘        
par    └─┘     └┘ └┘  └┘   └┘ └────────┘             └┘        
pid           └┘ └┘  └┘   └┘ └────────┘             └┘        
st   ────────────────────────────────┘└────────────────┘└────────┘└─
198    apply sqrt_two_add_series_step_up 23 16,
id           └─────────────────────────┘
src    └────┘└─────────────────────────┘└────┘
typ    └────┘└─────────────────────────┘└────┘
doc    └────┘                           └────┘
txt    └────┘                           └────┘
par    └────┘                           └────┘
pid                                    └──┘└┘
st   ────────────────────────────────────────┘└─
199    all_goals {norm_num}
src    └─────────┘└──────┘└┘
typ    └─────────┘└──────┘└┘
doc    └─────────┘└──────┘└┘
txt    └─────────┘└──────┘└┘
par    └─────────┘└──────┘└┘
pid             └─────────┘
st   ────────────┘└──────┘
200  end
st   └─┘
201  
202  lemma pi_gt_314 : pi > 3.14 :=
id                     └┘  
src                    └┘  
typ                    └┘  
doc                    └┘
203  begin
st   └─────
204    refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series 4), rw [mul_comm],
id            └────────────┘    └───────────────────────┘         └──────┘
src    └─────┘└────────────┘└─┘ └───────────────────────┘└─┘  └──┘└──────┘
typ    └─────┘└────────────┘└─┘ └───────────────────────┘└─┘  └──┘└──────┘
doc    └─────┘              └─┘                          └─┘  └──┘        
txt    └─────┘              └─┘                          └─┘  └──┘        
par    └─────┘              └─┘                          └─┘  └──┘        
pid                        └─┘                          └─┘    └┘        
st   ──────────────────────────────────────────────────────┘└────────────┘└──
205    apply le_mul_of_div_le, norm_num, apply le_sqrt_of_sqr_le,
id           └──────────────┘                  └───────────────┘
src    └────┘└──────────────┘  └──────┘  └────┘└───────────────┘
typ    └────┘└──────────────┘  └──────┘  └────┘└───────────────┘
doc    └────┘                  └──────┘  └────┘
txt    └────┘                  └──────┘  └────┘
par    └────┘                  └──────┘  └────┘
pid                                          
st   ───────────────────────┘└────────┘└───────────────────────┘└─
206    rw [le_sub, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
id         └────┘                                 └───────────┘  └──────┘
src    └──┘└────┘└┘     └┘ └┘ └┘  └┘ └────────┘└───────────┘└┘└──────┘└┘
typ    └──┘└────┘└┘     └┘ └┘ └┘  └┘ └────────┘└───────────┘└┘└──────┘└┘
doc    └──┘      └┘     └┘ └┘  └┘   └┘ └────────┘             └┘        └┘
txt    └──┘      └┘     └┘ └┘  └┘   └┘ └────────┘             └┘        └┘
par    └──┘      └┘     └┘ └┘  └┘   └┘ └────────┘             └┘        └┘
pid      └┘      └┘     └┘ └┘  └┘   └┘ └────────┘             └┘        └┘
st   ───────────┘└────────────────────────────┘└────────────────┘└────────┘└──
207    apply sqrt_two_add_series_step_up 99 70,
id           └─────────────────────────┘
src    └────┘└─────────────────────────┘└────┘
typ    └────┘└─────────────────────────┘└────┘
doc    └────┘                           └────┘
txt    └────┘                           └────┘
par    └────┘                           └────┘
pid                                    └──┘└┘
st   ────────────────────────────────────────┘└─
208    apply sqrt_two_add_series_step_up 874 473,
id           └─────────────────────────┘
src    └────┘└─────────────────────────┘└──────┘
typ    └────┘└─────────────────────────┘└──────┘
doc    └────┘                           └──────┘
txt    └────┘                           └──────┘
par    └────┘                           └──────┘
pid                                    └───┘└─┘
st   ──────────────────────────────────────────┘└─
209    apply sqrt_two_add_series_step_up 1940 989,
id           └─────────────────────────┘
src    └────┘└─────────────────────────┘└───────┘
typ    └────┘└─────────────────────────┘└───────┘
doc    └────┘                           └───────┘
txt    └────┘                           └───────┘
par    └────┘                           └───────┘
pid                                    └────┘└─┘
st   ───────────────────────────────────────────┘└─
210    apply sqrt_two_add_series_step_up 1447 727,
id           └─────────────────────────┘
src    └────┘└─────────────────────────┘└───────┘
typ    └────┘└─────────────────────────┘└───────┘
doc    └────┘                           └───────┘
txt    └────┘                           └───────┘
par    └────┘                           └───────┘
pid                                    └────┘└─┘
st   ───────────────────────────────────────────┘└─
211    all_goals {norm_num}
src    └─────────┘└──────┘└┘
typ    └─────────┘└──────┘└┘
doc    └─────────┘└──────┘└┘
txt    └─────────┘└──────┘└┘
par    └─────────┘└──────┘└┘
pid             └─────────┘
st   ────────────┘└──────┘
212  end
st   └─┘
213  
214  lemma pi_lt_315 : pi < 3.15 :=
id                     └┘  
src                    └┘  
typ                    └┘  
doc                    └┘
215  begin
st   └─────
216    refine lt_of_lt_of_le (pi_lt_sqrt_two_add_series 4) _,
id            └────────────┘  └───────────────────────┘
src    └─────┘└────────────┘ └───────────────────────┘└───┘
typ    └─────┘└────────────┘ └───────────────────────┘└───┘
doc    └─────┘                                        └───┘
txt    └─────┘                                        └───┘
par    └─────┘                                        └───┘
pid                                                  └───┘
st   ──────────────────────────────────────────────────────┘└─
217    apply add_le_of_le_sub_right, rw [mul_comm], apply mul_le_of_le_div, apply pow_pos, norm_num,
id           └────────────────────┘      └──────┘         └──────────────┘        └─────┘
src    └────┘└────────────────────┘  └──┘└──────┘  └────┘└──────────────┘  └────┘└─────┘  └──────┘
typ    └────┘└────────────────────┘  └──┘└──────┘  └────┘└──────────────┘  └────┘└─────┘  └──────┘
doc    └────┘                        └──┘          └────┘                  └────┘         └──────┘
txt    └────┘                        └──┘          └────┘                  └────┘         └──────┘
par    └────┘                        └──┘          └────┘                  └────┘         └──────┘
pid                                   └┘                                      
st   ─────────────────────────────┘└────────────┘└───────────────────────┘└─────────────┘└────────┘└─
218    rw [sqrt_le_left, sub_le, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
id         └──────────┘  └────┘                                 └───────────┘  └──────┘
src    └──┘└──────────┘└┘└────┘└┘     └┘ └┘ └┘  └┘ └────────┘└───────────┘└┘└──────┘└┘
typ    └──┘└──────────┘└┘└────┘└┘     └┘ └┘ └┘  └┘ └────────┘└───────────┘└┘└──────┘└┘
doc    └──┘            └┘      └┘     └┘ └┘  └┘   └┘ └────────┘             └┘        └┘
txt    └──┘            └┘      └┘     └┘ └┘  └┘   └┘ └────────┘             └┘        └┘
par    └──┘            └┘      └┘     └┘ └┘  └┘   └┘ └────────┘             └┘        └┘
pid      └┘            └┘      └┘     └┘ └┘  └┘   └┘ └────────┘             └┘        └┘
st   ─────────────────┘└──────┘└────────────────────────────┘└────────────────┘└────────┘└──
219    apply sqrt_two_add_series_step_down 140 99,
id           └───────────────────────────┘
src    └────┘└───────────────────────────┘└─────┘
typ    └────┘└───────────────────────────┘└─────┘
doc    └────┘                             └─────┘
txt    └────┘                             └─────┘
par    └────┘                             └─────┘
pid                                      └───┘└┘
st   ───────────────────────────────────────────┘└─
220    apply sqrt_two_add_series_step_down 279 151,
id           └───────────────────────────┘
src    └────┘└───────────────────────────┘└──────┘
typ    └────┘└───────────────────────────┘└──────┘
doc    └────┘                             └──────┘
txt    └────┘                             └──────┘
par    └────┘                             └──────┘
pid                                      └───┘└─┘
st   ────────────────────────────────────────────┘└─
221    apply sqrt_two_add_series_step_down 51 26,
id           └───────────────────────────┘
src    └────┘└───────────────────────────┘└────┘
typ    └────┘└───────────────────────────┘└────┘
doc    └────┘                             └────┘
txt    └────┘                             └────┘
par    └────┘                             └────┘
pid                                      └──┘└┘
st   ──────────────────────────────────────────┘└─
222    apply sqrt_two_add_series_step_down 412 207,
id           └───────────────────────────┘
src    └────┘└───────────────────────────┘└──────┘
typ    └────┘└───────────────────────────┘└──────┘
doc    └────┘                             └──────┘
txt    └────┘                             └──────┘
par    └────┘                             └──────┘
pid                                      └───┘└─┘
st   ────────────────────────────────────────────┘└─
223    all_goals {norm_num}
src    └─────────┘└──────┘└┘
typ    └─────────┘└──────┘└┘
doc    └─────────┘└──────┘└┘
txt    └─────────┘└──────┘└┘
par    └─────────┘└──────┘└┘
pid             └─────────┘
st   ────────────┘└──────┘
224  end
st   └─┘
225  
226  /- A computation of the first 7 digits of pi is given here:
227    <https://gist.github.com/fpvandoorn/5b405988bc2e61953d56e3597db16ecf>
228    This is not included in mathlib, because of slow compilation time.
229    -/
230  
231  end real